\begin{tabbing}
$\forall$\=$i$, $x$:Id, $k$:Knd, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$a$:Knd fp$\rightarrow$ Type,\+
\\[0ex]$f$:(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$${\it ds}$($x$)?Void).
\-\\[0ex]@$i$: with declarations ds:${\it ds}$da:${\it da}$effect of $k$(v) is $x$ := $f$ s v $\in$ Dsys
\end{tabbing}